Inference at * 1 2 1 
Iof proof for Lemma adjacent-cons:



1. T : Type
2. x : T
3. y : T
4. u : T
5. L : T List
6. i : {0..((||L||+1) - 1)}
7. x = [u / L][i]
8. y = [u / L][(i+1)]
9. 0 < ||L||
10. (i = 0)
  x = L[(i - 1)] 

latex

 by ((RWO "select_cons_tl" (-4)) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	l[i], P  Q, P & Q, x:A  B(x), P  Q, x:A. B(x), s = t, P  Q, x:AB(x)
Lemmas	iff wf, rev implies wf, select cons tl